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  2453  2reu1  3851  frpoinsg  6295  ordunidif  6361  isofrlem  7281  dfwe2  7714  orduniorsuc  7769  tfisg  7794  poxp  8068  fnse  8073  ssenen  9075  dffi3  9340  fpwwe2lem12  10555  zmulcl  12543  rpneg  12946  rexuz3  15275  cau3lem  15281  climrlim2  15473  o1rlimmul  15545  iseralt  15611  gcdzeq  16482  isprm3  16613  vdwnnlem2  16927  ablfaclem3  19987  epttop  22913  lmcnp  23208  dfconn2  23323  txcnp  23524  cmphaushmeo  23704  isfild  23762  cnpflf2  23904  flimfnfcls  23932  alexsubALT  23955  fgcfil  25188  bcthlem5  25245  ivthlem2  25370  ivthlem3  25371  dvfsumrlim  25955  plypf1  26134  noetalem1  27670  noseqinds  28211  axeuclidlem  28926  usgr2wlkneq  29720  wwlksnredwwlkn0  29860  wwlksnextwrd  29861  clwlkclwwlklem2a1  29955  lnon0  30761  hstles  32194  mdsl1i  32284  atcveq0  32311  atcvat4i  32360  cdjreui  32395  issgon  34109  connpconn  35227  outsideofrflx  36120  isbasisrelowllem1  37348  isbasisrelowllem2  37349  poimirlem3  37622  poimirlem29  37648  poimir  37652  heicant  37654  equivtotbnd  37777  ismtybndlem  37805  cvrat4  39442  linepsubN  39751  pmapsub  39767  osumcllem4N  39958  pexmidlem1N  39969  dochexmidlem1  41459  cantnfresb  43317  harval3  43531  clcnvlem  43616  relpfrlem  44947  iccpartimp  47421  sbgoldbwt  47781  sbgoldbst  47782  elsetrecslem  49704