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  2463  2reu1  3919  frpoinsg  6375  ordunidif  6444  isofrlem  7376  dfwe2  7809  orduniorsuc  7866  tfisg  7891  poxp  8169  fnse  8174  ssenen  9217  dffi3  9500  fpwwe2lem12  10711  zmulcl  12692  rpneg  13089  rexuz3  15397  cau3lem  15403  climrlim2  15593  o1rlimmul  15665  iseralt  15733  gcdzeq  16599  isprm3  16730  vdwnnlem2  17043  ablfaclem3  20131  epttop  23037  lmcnp  23333  dfconn2  23448  txcnp  23649  cmphaushmeo  23829  isfild  23887  cnpflf2  24029  flimfnfcls  24057  alexsubALT  24080  fgcfil  25324  bcthlem5  25381  ivthlem2  25506  ivthlem3  25507  dvfsumrlim  26092  plypf1  26271  noetalem1  27804  noseqinds  28317  axeuclidlem  28995  usgr2wlkneq  29792  wwlksnredwwlkn0  29929  wwlksnextwrd  29930  clwlkclwwlklem2a1  30024  lnon0  30830  hstles  32263  mdsl1i  32353  atcveq0  32380  atcvat4i  32429  cdjreui  32464  issgon  34087  connpconn  35203  outsideofrflx  36091  isbasisrelowllem1  37321  isbasisrelowllem2  37322  poimirlem3  37583  poimirlem29  37609  poimir  37613  heicant  37615  equivtotbnd  37738  ismtybndlem  37766  cvrat4  39400  linepsubN  39709  pmapsub  39725  osumcllem4N  39916  pexmidlem1N  39927  dochexmidlem1  41417  cantnfresb  43286  harval3  43500  clcnvlem  43585  iccpartimp  47291  sbgoldbwt  47651  sbgoldbst  47652  elsetrecslem  48791