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  2454  2reu1  3863  frpoinsg  6319  ordunidif  6385  isofrlem  7318  dfwe2  7753  orduniorsuc  7808  tfisg  7833  poxp  8110  fnse  8115  ssenen  9121  dffi3  9389  fpwwe2lem12  10602  zmulcl  12589  rpneg  12992  rexuz3  15322  cau3lem  15328  climrlim2  15520  o1rlimmul  15592  iseralt  15658  gcdzeq  16529  isprm3  16660  vdwnnlem2  16974  ablfaclem3  20026  epttop  22903  lmcnp  23198  dfconn2  23313  txcnp  23514  cmphaushmeo  23694  isfild  23752  cnpflf2  23894  flimfnfcls  23922  alexsubALT  23945  fgcfil  25178  bcthlem5  25235  ivthlem2  25360  ivthlem3  25361  dvfsumrlim  25945  plypf1  26124  noetalem1  27660  noseqinds  28194  axeuclidlem  28896  usgr2wlkneq  29693  wwlksnredwwlkn0  29833  wwlksnextwrd  29834  clwlkclwwlklem2a1  29928  lnon0  30734  hstles  32167  mdsl1i  32257  atcveq0  32284  atcvat4i  32333  cdjreui  32368  issgon  34120  connpconn  35229  outsideofrflx  36122  isbasisrelowllem1  37350  isbasisrelowllem2  37351  poimirlem3  37624  poimirlem29  37650  poimir  37654  heicant  37656  equivtotbnd  37779  ismtybndlem  37807  cvrat4  39444  linepsubN  39753  pmapsub  39769  osumcllem4N  39960  pexmidlem1N  39971  dochexmidlem1  41461  cantnfresb  43320  harval3  43534  clcnvlem  43619  relpfrlem  44950  iccpartimp  47422  sbgoldbwt  47782  sbgoldbst  47783  elsetrecslem  49692