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  2457  2reu1  3905  frpoinsg  6365  ordunidif  6434  isofrlem  7359  dfwe2  7792  orduniorsuc  7849  tfisg  7874  poxp  8151  fnse  8156  ssenen  9189  dffi3  9468  fpwwe2lem12  10679  zmulcl  12663  rpneg  13064  rexuz3  15383  cau3lem  15389  climrlim2  15579  o1rlimmul  15651  iseralt  15717  gcdzeq  16585  isprm3  16716  vdwnnlem2  17029  ablfaclem3  20121  epttop  23031  lmcnp  23327  dfconn2  23442  txcnp  23643  cmphaushmeo  23823  isfild  23881  cnpflf2  24023  flimfnfcls  24051  alexsubALT  24074  fgcfil  25318  bcthlem5  25375  ivthlem2  25500  ivthlem3  25501  dvfsumrlim  26086  plypf1  26265  noetalem1  27800  noseqinds  28313  axeuclidlem  28991  usgr2wlkneq  29788  wwlksnredwwlkn0  29925  wwlksnextwrd  29926  clwlkclwwlklem2a1  30020  lnon0  30826  hstles  32259  mdsl1i  32349  atcveq0  32376  atcvat4i  32425  cdjreui  32460  issgon  34103  connpconn  35219  outsideofrflx  36108  isbasisrelowllem1  37337  isbasisrelowllem2  37338  poimirlem3  37609  poimirlem29  37635  poimir  37639  heicant  37641  equivtotbnd  37764  ismtybndlem  37792  cvrat4  39425  linepsubN  39734  pmapsub  39750  osumcllem4N  39941  pexmidlem1N  39952  dochexmidlem1  41442  cantnfresb  43313  harval3  43527  clcnvlem  43612  iccpartimp  47341  sbgoldbwt  47701  sbgoldbst  47702  elsetrecslem  48929