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  2458  2reu1  3877  frpoinsg  6343  ordunidif  6413  isofrlem  7342  dfwe2  7776  orduniorsuc  7832  tfisg  7857  poxp  8135  fnse  8140  ssenen  9173  dffi3  9453  fpwwe2lem12  10664  zmulcl  12649  rpneg  13049  rexuz3  15369  cau3lem  15375  climrlim2  15565  o1rlimmul  15637  iseralt  15703  gcdzeq  16571  isprm3  16702  vdwnnlem2  17016  ablfaclem3  20075  epttop  22963  lmcnp  23258  dfconn2  23373  txcnp  23574  cmphaushmeo  23754  isfild  23812  cnpflf2  23954  flimfnfcls  23982  alexsubALT  24005  fgcfil  25241  bcthlem5  25298  ivthlem2  25423  ivthlem3  25424  dvfsumrlim  26008  plypf1  26187  noetalem1  27722  noseqinds  28235  axeuclidlem  28907  usgr2wlkneq  29704  wwlksnredwwlkn0  29844  wwlksnextwrd  29845  clwlkclwwlklem2a1  29939  lnon0  30745  hstles  32178  mdsl1i  32268  atcveq0  32295  atcvat4i  32344  cdjreui  32379  issgon  34083  connpconn  35199  outsideofrflx  36087  isbasisrelowllem1  37315  isbasisrelowllem2  37316  poimirlem3  37589  poimirlem29  37615  poimir  37619  heicant  37621  equivtotbnd  37744  ismtybndlem  37772  cvrat4  39404  linepsubN  39713  pmapsub  39729  osumcllem4N  39920  pexmidlem1N  39931  dochexmidlem1  41421  cantnfresb  43299  harval3  43513  clcnvlem  43598  relpfrlem  44931  iccpartimp  47362  sbgoldbwt  47722  sbgoldbst  47723  elsetrecslem  49226