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  3836  frpoinsg  6301  ordunidif  6367  isofrlem  7288  dfwe2  7721  orduniorsuc  7774  tfisg  7798  poxp  8071  fnse  8076  ssenen  9082  dffi3  9337  fpwwe2lem12  10556  zmulcl  12567  rpneg  12967  rexuz3  15302  cau3lem  15308  climrlim2  15500  o1rlimmul  15572  iseralt  15638  gcdzeq  16512  isprm3  16643  vdwnnlem2  16958  chnccat  18583  ablfaclem3  20055  epttop  22984  lmcnp  23279  dfconn2  23394  txcnp  23595  cmphaushmeo  23775  isfild  23833  cnpflf2  23975  flimfnfcls  24003  alexsubALT  24026  fgcfil  25248  bcthlem5  25305  ivthlem2  25429  ivthlem3  25430  dvfsumrlim  26008  plypf1  26187  noetalem1  27719  noseqinds  28299  axeuclidlem  29045  usgr2wlkneq  29839  wwlksnredwwlkn0  29979  wwlksnextwrd  29980  clwlkclwwlklem2a1  30077  lnon0  30884  hstles  32317  mdsl1i  32407  atcveq0  32434  atcvat4i  32483  cdjreui  32518  issgon  34283  connpconn  35433  outsideofrflx  36325  isbasisrelowllem1  37685  isbasisrelowllem2  37686  poimirlem3  37958  poimirlem29  37984  poimir  37988  heicant  37990  equivtotbnd  38113  ismtybndlem  38141  cvrat4  39903  linepsubN  40212  pmapsub  40228  osumcllem4N  40419  pexmidlem1N  40430  dochexmidlem1  41920  cantnfresb  43770  harval3  43983  clcnvlem  44068  relpfrlem  45398  iccpartimp  47889  sbgoldbwt  48265  sbgoldbst  48266  elsetrecslem  50186