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  3835  frpoinsg  6307  ordunidif  6373  isofrlem  7295  dfwe2  7728  orduniorsuc  7781  tfisg  7805  poxp  8078  fnse  8083  ssenen  9089  dffi3  9344  fpwwe2lem12  10565  zmulcl  12576  rpneg  12976  rexuz3  15311  cau3lem  15317  climrlim2  15509  o1rlimmul  15581  iseralt  15647  gcdzeq  16521  isprm3  16652  vdwnnlem2  16967  chnccat  18592  ablfaclem3  20064  epttop  22974  lmcnp  23269  dfconn2  23384  txcnp  23585  cmphaushmeo  23765  isfild  23823  cnpflf2  23965  flimfnfcls  23993  alexsubALT  24016  fgcfil  25238  bcthlem5  25295  ivthlem2  25419  ivthlem3  25420  dvfsumrlim  25998  plypf1  26177  noetalem1  27705  noseqinds  28285  axeuclidlem  29031  usgr2wlkneq  29824  wwlksnredwwlkn0  29964  wwlksnextwrd  29965  clwlkclwwlklem2a1  30062  lnon0  30869  hstles  32302  mdsl1i  32392  atcveq0  32419  atcvat4i  32468  cdjreui  32503  issgon  34267  connpconn  35417  outsideofrflx  36309  isbasisrelowllem1  37671  isbasisrelowllem2  37672  poimirlem3  37944  poimirlem29  37970  poimir  37974  heicant  37976  equivtotbnd  38099  ismtybndlem  38127  cvrat4  39889  linepsubN  40198  pmapsub  40214  osumcllem4N  40405  pexmidlem1N  40416  dochexmidlem1  41906  cantnfresb  43752  harval3  43965  clcnvlem  44050  relpfrlem  45380  iccpartimp  47877  sbgoldbwt  48253  sbgoldbst  48254  elsetrecslem  50174