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  2453  2reu1  3851  frpoinsg  6295  ordunidif  6361  isofrlem  7281  dfwe2  7714  orduniorsuc  7769  tfisg  7794  poxp  8068  fnse  8073  ssenen  9075  dffi3  9340  fpwwe2lem12  10555  zmulcl  12542  rpneg  12945  rexuz3  15274  cau3lem  15280  climrlim2  15472  o1rlimmul  15544  iseralt  15610  gcdzeq  16481  isprm3  16612  vdwnnlem2  16926  ablfaclem3  19986  epttop  22912  lmcnp  23207  dfconn2  23322  txcnp  23523  cmphaushmeo  23703  isfild  23761  cnpflf2  23903  flimfnfcls  23931  alexsubALT  23954  fgcfil  25187  bcthlem5  25244  ivthlem2  25369  ivthlem3  25370  dvfsumrlim  25954  plypf1  26133  noetalem1  27669  noseqinds  28210  axeuclidlem  28925  usgr2wlkneq  29719  wwlksnredwwlkn0  29859  wwlksnextwrd  29860  clwlkclwwlklem2a1  29954  lnon0  30760  hstles  32193  mdsl1i  32283  atcveq0  32310  atcvat4i  32359  cdjreui  32394  issgon  34092  connpconn  35210  outsideofrflx  36103  isbasisrelowllem1  37331  isbasisrelowllem2  37332  poimirlem3  37605  poimirlem29  37631  poimir  37635  heicant  37637  equivtotbnd  37760  ismtybndlem  37788  cvrat4  39425  linepsubN  39734  pmapsub  39750  osumcllem4N  39941  pexmidlem1N  39952  dochexmidlem1  41442  cantnfresb  43300  harval3  43514  clcnvlem  43599  relpfrlem  44930  iccpartimp  47405  sbgoldbwt  47765  sbgoldbst  47766  elsetrecslem  49688