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 206  df-an 396

This theorem is referenced by:  anc2li  555  equvini  2456  2reu1  3834  frpoinsg  6243  ordunidif  6311  isofrlem  7204  dfwe2  7615  orduniorsuc  7665  poxp  7953  fnse  7958  ssenen  8903  dffi3  9151  frminOLD  9491  fpwwe2lem12  10382  zmulcl  12352  rpneg  12744  rexuz3  15041  cau3lem  15047  climrlim2  15237  o1rlimmul  15309  iseralt  15377  gcdzeq  16243  isprm3  16369  vdwnnlem2  16678  ablfaclem3  19671  epttop  22140  lmcnp  22436  dfconn2  22551  txcnp  22752  cmphaushmeo  22932  isfild  22990  cnpflf2  23132  flimfnfcls  23160  alexsubALT  23183  fgcfil  24416  bcthlem5  24473  ivthlem2  24597  ivthlem3  24598  dvfsumrlim  25176  plypf1  25354  axeuclidlem  27311  usgr2wlkneq  28103  wwlksnredwwlkn0  28240  wwlksnextwrd  28241  clwlkclwwlklem2a1  28335  lnon0  29139  hstles  30572  mdsl1i  30662  atcveq0  30689  atcvat4i  30738  cdjreui  30773  issgon  32070  connpconn  33176  tfisg  33765  noetalem1  33923  outsideofrflx  34408  isbasisrelowllem1  35505  isbasisrelowllem2  35506  poimirlem3  35759  poimirlem29  35785  poimir  35789  heicant  35791  equivtotbnd  35915  ismtybndlem  35943  cvrat4  37436  linepsubN  37745  pmapsub  37761  osumcllem4N  37952  pexmidlem1N  37963  dochexmidlem1  39453  harval3  41105  clcnvlem  41184  iccpartimp  44821  sbgoldbwt  45181  sbgoldbst  45182  elsetrecslem  46356