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 207  df-an 396

This theorem is referenced by:  anc2li  555  equvini  2460  2reu1  3897  frpoinsg  6364  ordunidif  6433  isofrlem  7360  dfwe2  7794  orduniorsuc  7850  tfisg  7875  poxp  8153  fnse  8158  ssenen  9191  dffi3  9471  fpwwe2lem12  10682  zmulcl  12666  rpneg  13067  rexuz3  15387  cau3lem  15393  climrlim2  15583  o1rlimmul  15655  iseralt  15721  gcdzeq  16589  isprm3  16720  vdwnnlem2  17034  ablfaclem3  20107  epttop  23016  lmcnp  23312  dfconn2  23427  txcnp  23628  cmphaushmeo  23808  isfild  23866  cnpflf2  24008  flimfnfcls  24036  alexsubALT  24059  fgcfil  25305  bcthlem5  25362  ivthlem2  25487  ivthlem3  25488  dvfsumrlim  26072  plypf1  26251  noetalem1  27786  noseqinds  28299  axeuclidlem  28977  usgr2wlkneq  29776  wwlksnredwwlkn0  29916  wwlksnextwrd  29917  clwlkclwwlklem2a1  30011  lnon0  30817  hstles  32250  mdsl1i  32340  atcveq0  32367  atcvat4i  32416  cdjreui  32451  issgon  34124  connpconn  35240  outsideofrflx  36128  isbasisrelowllem1  37356  isbasisrelowllem2  37357  poimirlem3  37630  poimirlem29  37656  poimir  37660  heicant  37662  equivtotbnd  37785  ismtybndlem  37813  cvrat4  39445  linepsubN  39754  pmapsub  39770  osumcllem4N  39961  pexmidlem1N  39972  dochexmidlem1  41462  cantnfresb  43337  harval3  43551  clcnvlem  43636  relpfrlem  44974  iccpartimp  47404  sbgoldbwt  47764  sbgoldbst  47765  elsetrecslem  49218