Theorem jctild 525

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctild.1	⊢ (𝜑 → (𝜓 → 𝜒))
jctild.2	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jctild	⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 512	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  anc2li  555  equvini  2449  2reu1  3887  frpoinsg  6343  ordunidif  6412  isofrlem  7342  dfwe2  7770  orduniorsuc  7827  tfisg  7852  poxp  8127  fnse  8132  ssenen  9169  dffi3  9448  fpwwe2lem12  10659  zmulcl  12635  rpneg  13032  rexuz3  15321  cau3lem  15327  climrlim2  15517  o1rlimmul  15589  iseralt  15657  gcdzeq  16521  isprm3  16647  vdwnnlem2  16958  ablfaclem3  20037  epttop  22905  lmcnp  23201  dfconn2  23316  txcnp  23517  cmphaushmeo  23697  isfild  23755  cnpflf2  23897  flimfnfcls  23925  alexsubALT  23948  fgcfil  25192  bcthlem5  25249  ivthlem2  25374  ivthlem3  25375  dvfsumrlim  25959  plypf1  26139  noetalem1  27667  noseqinds  28159  axeuclidlem  28766  usgr2wlkneq  29563  wwlksnredwwlkn0  29700  wwlksnextwrd  29701  clwlkclwwlklem2a1  29795  lnon0  30601  hstles  32034  mdsl1i  32124  atcveq0  32151  atcvat4i  32200  cdjreui  32235  issgon  33732  connpconn  34835  outsideofrflx  35713  isbasisrelowllem1  36824  isbasisrelowllem2  36825  poimirlem3  37085  poimirlem29  37111  poimir  37115  heicant  37117  equivtotbnd  37240  ismtybndlem  37268  cvrat4  38905  linepsubN  39214  pmapsub  39230  osumcllem4N  39421  pexmidlem1N  39432  dochexmidlem1  40922  cantnfresb  42725  harval3  42940  clcnvlem  43025  iccpartimp  46729  sbgoldbwt  47089  sbgoldbst  47090  elsetrecslem  48102