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  3849  frpoinsg  6309  ordunidif  6375  isofrlem  7296  dfwe2  7729  orduniorsuc  7782  tfisg  7806  poxp  8080  fnse  8085  ssenen  9091  dffi3  9346  fpwwe2lem12  10565  zmulcl  12552  rpneg  12951  rexuz3  15284  cau3lem  15290  climrlim2  15482  o1rlimmul  15554  iseralt  15620  gcdzeq  16491  isprm3  16622  vdwnnlem2  16936  chnccat  18561  ablfaclem3  20030  epttop  22965  lmcnp  23260  dfconn2  23375  txcnp  23576  cmphaushmeo  23756  isfild  23814  cnpflf2  23956  flimfnfcls  23984  alexsubALT  24007  fgcfil  25239  bcthlem5  25296  ivthlem2  25421  ivthlem3  25422  dvfsumrlim  26006  plypf1  26185  noetalem1  27721  noseqinds  28301  axeuclidlem  29047  usgr2wlkneq  29841  wwlksnredwwlkn0  29981  wwlksnextwrd  29982  clwlkclwwlklem2a1  30079  lnon0  30885  hstles  32318  mdsl1i  32408  atcveq0  32435  atcvat4i  32484  cdjreui  32519  issgon  34300  connpconn  35448  outsideofrflx  36340  isbasisrelowllem1  37607  isbasisrelowllem2  37608  poimirlem3  37871  poimirlem29  37897  poimir  37901  heicant  37903  equivtotbnd  38026  ismtybndlem  38054  cvrat4  39816  linepsubN  40125  pmapsub  40141  osumcllem4N  40332  pexmidlem1N  40343  dochexmidlem1  41833  cantnfresb  43678  harval3  43891  clcnvlem  43976  relpfrlem  45306  iccpartimp  47774  sbgoldbwt  48134  sbgoldbst  48135  elsetrecslem  50055