Theorem jctild 523

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anc2li  553  syl6an  676  ordunidif  6011  isofrlem  6845  dfwe2  7242  orduniorsuc  7291  poxp  7553  fnse  7558  ssenen  8403  dffi3  8606  fpwwe2lem13  9779  zmulcl  11754  rpneg  12146  rexuz3  14465  cau3lem  14471  climrlim2  14655  o1rlimmul  14726  iseralt  14792  gcdzeq  15644  isprm3  15768  vdwnnlem2  16071  ablfaclem3  18840  epttop  21184  lmcnp  21479  dfconn2  21593  txcnp  21794  cmphaushmeo  21974  isfild  22032  cnpflf2  22174  flimfnfcls  22202  alexsubALT  22225  fgcfil  23439  bcthlem5  23496  ivthlem2  23618  ivthlem3  23619  dvfsumrlim  24193  plypf1  24367  axeuclidlem  26261  usgr2wlkneq  27058  wwlksnredwwlkn0  27209  wwlksnredwwlkn0OLD  27210  wwlksnextwrd  27211  wwlksnextwrdOLD  27216  clwlkclwwlklem2a1  27321  lnon0  28208  hstles  29645  mdsl1i  29735  atcveq0  29762  atcvat4i  29811  cdjreui  29846  issgon  30731  connpconn  31763  tfisg  32254  frpoinsg  32280  frmin  32281  outsideofrflx  32773  isbasisrelowllem1  33748  isbasisrelowllem2  33749  poimirlem3  33956  poimirlem29  33982  poimir  33986  heicant  33988  equivtotbnd  34119  ismtybndlem  34147  cvrat4  35518  linepsubN  35827  pmapsub  35843  osumcllem4N  36034  pexmidlem1N  36045  dochexmidlem1  37535  clcnvlem  38771  2reu1  42011  iccpartimp  42241  sbgoldbwt  42495  sbgoldbst  42496  elsetrecslem  43340