Theorem jctild 566

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 555	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  syl6an  568  anc2li  580  ordunidif  5773  isofrlem  6590  dfwe2  6981  orduniorsuc  7030  poxp  7289  fnse  7294  ssenen  8134  dffi3  8337  fpwwe2lem13  9464  zmulcl  11426  rpneg  11863  rexuz3  14088  cau3lem  14094  climrlim2  14278  o1rlimmul  14349  iseralt  14415  gcdzeq  15271  isprm3  15396  vdwnnlem2  15700  ablfaclem3  18486  epttop  20813  lmcnp  21108  dfconn2  21222  txcnp  21423  cmphaushmeo  21603  isfild  21662  cnpflf2  21804  flimfnfcls  21832  alexsubALT  21855  fgcfil  23069  bcthlem5  23125  ivthlem2  23221  ivthlem3  23222  dvfsumrlim  23794  plypf1  23968  axeuclidlem  25842  usgr2wlkneq  26652  wwlksnredwwlkn0  26791  wwlksnextwrd  26792  wwlksnextproplem1  26804  clwlkclwwlklem2a1  26893  numclwwlkovf2exlem2  27212  extwwlkfab  27223  lnon0  27653  hstles  29090  mdsl1i  29180  atcveq0  29207  atcvat4i  29256  cdjreui  29291  issgon  30186  connpconn  31217  tfisg  31716  frmin  31739  outsideofrflx  32234  isbasisrelowllem1  33203  isbasisrelowllem2  33204  poimirlem3  33412  poimirlem29  33438  poimir  33442  heicant  33444  equivtotbnd  33577  ismtybndlem  33605  cvrat4  34729  linepsubN  35038  pmapsub  35054  osumcllem4N  35245  pexmidlem1N  35256  dochexmidlem1  36749  clcnvlem  37930  2reu1  41186  iccpartimp  41353  sbgoldbwt  41665  sbgoldbst  41666  elsetrecslem  42444