Theorem jctild 564

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  syl6an  566  anc2li  578  ordunidif  5690  isofrlem  6490  dfwe2  6873  orduniorsuc  6922  poxp  7176  fnse  7181  ssenen  8019  dffi3  8220  fpwwe2lem13  9343  zmulcl  11303  rpneg  11739  rexuz3  13936  cau3lem  13942  climrlim2  14126  o1rlimmul  14197  iseralt  14263  gcdzeq  15109  isprm3  15234  vdwnnlem2  15538  ablfaclem3  18309  epttop  20623  lmcnp  20918  dfcon2  21032  txcnp  21233  cmphaushmeo  21413  isfild  21472  cnpflf2  21614  flimfnfcls  21642  alexsubALT  21665  fgcfil  22877  bcthlem5  22933  ivthlem2  23028  ivthlem3  23029  dvfsumrlim  23598  plypf1  23772  axeuclidlem  25642  wwlknredwwlkn0  26255  wwlkextwrd  26256  wwlkextproplem1  26269  clwlkisclwwlklem2a1  26307  rusgranumwlklem1  26476  numclwwlkovf2ex  26613  extwwlkfab  26617  lnon0  27037  hstles  28474  mdsl1i  28564  atcveq0  28591  atcvat4i  28640  cdjreui  28675  issgon  29513  conpcon  30471  tfisg  30960  frmin  30983  outsideofrflx  31404  isbasisrelowllem1  32379  isbasisrelowllem2  32380  poimirlem3  32582  poimirlem29  32608  poimir  32612  heicant  32614  equivtotbnd  32747  ismtybndlem  32775  cvrat4  33747  linepsubN  34056  pmapsub  34072  osumcllem4N  34263  pexmidlem1N  34274  dochexmidlem1  35767  clcnvlem  36949  2reu1  39835  iccpartimp  39955  bgoldbwt  40199  bgoldbst  40200  usgr2wlkneq  40962  wwlksnredwwlkn0  41102  wwlksnextwrd  41103  wwlksnextproplem1  41115  clwlkclwwlklem2a1  41201  av-numclwwlkovf2ex  41517  av-extwwlkfab  41520  elsetrecslem  42243