Theorem jctild 565

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

This theorem is referenced by:  syl6an  567  anc2li  579  ordunidif  5811  isofrlem  6630  dfwe2  7023  orduniorsuc  7072  poxp  7334  fnse  7339  ssenen  8175  dffi3  8378  fpwwe2lem13  9502  zmulcl  11464  rpneg  11901  rexuz3  14132  cau3lem  14138  climrlim2  14322  o1rlimmul  14393  iseralt  14459  gcdzeq  15318  isprm3  15443  vdwnnlem2  15747  ablfaclem3  18532  epttop  20861  lmcnp  21156  dfconn2  21270  txcnp  21471  cmphaushmeo  21651  isfild  21709  cnpflf2  21851  flimfnfcls  21879  alexsubALT  21902  fgcfil  23115  bcthlem5  23171  ivthlem2  23267  ivthlem3  23268  dvfsumrlim  23839  plypf1  24013  axeuclidlem  25887  usgr2wlkneq  26708  wwlksnredwwlkn0  26859  wwlksnextwrd  26860  clwlkclwwlklem2a1  26958  extwwlkfab  27342  lnon0  27781  hstles  29218  mdsl1i  29308  atcveq0  29335  atcvat4i  29384  cdjreui  29419  issgon  30314  connpconn  31343  tfisg  31840  frpoinsg  31866  frmin  31867  outsideofrflx  32359  isbasisrelowllem1  33333  isbasisrelowllem2  33334  poimirlem3  33542  poimirlem29  33568  poimir  33572  heicant  33574  equivtotbnd  33707  ismtybndlem  33735  cvrat4  35047  linepsubN  35356  pmapsub  35372  osumcllem4N  35563  pexmidlem1N  35574  dochexmidlem1  37066  clcnvlem  38247  2reu1  41507  iccpartimp  41678  sbgoldbwt  41990  sbgoldbst  41991  elsetrecslem  42770