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  2459  2reu1  3872  frpoinsg  6332  ordunidif  6402  isofrlem  7332  dfwe2  7766  orduniorsuc  7822  tfisg  7847  poxp  8125  fnse  8130  ssenen  9163  dffi3  9441  fpwwe2lem12  10654  zmulcl  12639  rpneg  13039  rexuz3  15365  cau3lem  15371  climrlim2  15561  o1rlimmul  15633  iseralt  15699  gcdzeq  16569  isprm3  16700  vdwnnlem2  17014  ablfaclem3  20068  epttop  22945  lmcnp  23240  dfconn2  23355  txcnp  23556  cmphaushmeo  23736  isfild  23794  cnpflf2  23936  flimfnfcls  23964  alexsubALT  23987  fgcfil  25221  bcthlem5  25278  ivthlem2  25403  ivthlem3  25404  dvfsumrlim  25988  plypf1  26167  noetalem1  27703  noseqinds  28216  axeuclidlem  28887  usgr2wlkneq  29684  wwlksnredwwlkn0  29824  wwlksnextwrd  29825  clwlkclwwlklem2a1  29919  lnon0  30725  hstles  32158  mdsl1i  32248  atcveq0  32275  atcvat4i  32324  cdjreui  32359  issgon  34100  connpconn  35203  outsideofrflx  36091  isbasisrelowllem1  37319  isbasisrelowllem2  37320  poimirlem3  37593  poimirlem29  37619  poimir  37623  heicant  37625  equivtotbnd  37748  ismtybndlem  37776  cvrat4  39408  linepsubN  39717  pmapsub  39733  osumcllem4N  39924  pexmidlem1N  39935  dochexmidlem1  41425  cantnfresb  43295  harval3  43509  clcnvlem  43594  relpfrlem  44926  iccpartimp  47379  sbgoldbwt  47739  sbgoldbst  47740  elsetrecslem  49511