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  3847  frpoinsg  6301  ordunidif  6367  isofrlem  7286  dfwe2  7719  orduniorsuc  7772  tfisg  7796  poxp  8070  fnse  8075  ssenen  9079  dffi3  9334  fpwwe2lem12  10553  zmulcl  12540  rpneg  12939  rexuz3  15272  cau3lem  15278  climrlim2  15470  o1rlimmul  15542  iseralt  15608  gcdzeq  16479  isprm3  16610  vdwnnlem2  16924  chnccat  18549  ablfaclem3  20018  epttop  22953  lmcnp  23248  dfconn2  23363  txcnp  23564  cmphaushmeo  23744  isfild  23802  cnpflf2  23944  flimfnfcls  23972  alexsubALT  23995  fgcfil  25227  bcthlem5  25284  ivthlem2  25409  ivthlem3  25410  dvfsumrlim  25994  plypf1  26173  noetalem1  27709  noseqinds  28289  axeuclidlem  29035  usgr2wlkneq  29829  wwlksnredwwlkn0  29969  wwlksnextwrd  29970  clwlkclwwlklem2a1  30067  lnon0  30873  hstles  32306  mdsl1i  32396  atcveq0  32423  atcvat4i  32472  cdjreui  32507  issgon  34280  connpconn  35429  outsideofrflx  36321  isbasisrelowllem1  37560  isbasisrelowllem2  37561  poimirlem3  37824  poimirlem29  37850  poimir  37854  heicant  37856  equivtotbnd  37979  ismtybndlem  38007  cvrat4  39703  linepsubN  40012  pmapsub  40028  osumcllem4N  40219  pexmidlem1N  40230  dochexmidlem1  41720  cantnfresb  43566  harval3  43779  clcnvlem  43864  relpfrlem  45194  iccpartimp  47663  sbgoldbwt  48023  sbgoldbst  48024  elsetrecslem  49944