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  3857  frpoinsg  6304  ordunidif  6370  isofrlem  7297  dfwe2  7730  orduniorsuc  7785  tfisg  7810  poxp  8084  fnse  8089  ssenen  9092  dffi3  9358  fpwwe2lem12  10571  zmulcl  12558  rpneg  12961  rexuz3  15291  cau3lem  15297  climrlim2  15489  o1rlimmul  15561  iseralt  15627  gcdzeq  16498  isprm3  16629  vdwnnlem2  16943  ablfaclem3  19995  epttop  22872  lmcnp  23167  dfconn2  23282  txcnp  23483  cmphaushmeo  23663  isfild  23721  cnpflf2  23863  flimfnfcls  23891  alexsubALT  23914  fgcfil  25147  bcthlem5  25204  ivthlem2  25329  ivthlem3  25330  dvfsumrlim  25914  plypf1  26093  noetalem1  27629  noseqinds  28163  axeuclidlem  28865  usgr2wlkneq  29659  wwlksnredwwlkn0  29799  wwlksnextwrd  29800  clwlkclwwlklem2a1  29894  lnon0  30700  hstles  32133  mdsl1i  32223  atcveq0  32250  atcvat4i  32299  cdjreui  32334  issgon  34086  connpconn  35195  outsideofrflx  36088  isbasisrelowllem1  37316  isbasisrelowllem2  37317  poimirlem3  37590  poimirlem29  37616  poimir  37620  heicant  37622  equivtotbnd  37745  ismtybndlem  37773  cvrat4  39410  linepsubN  39719  pmapsub  39735  osumcllem4N  39926  pexmidlem1N  39937  dochexmidlem1  41427  cantnfresb  43286  harval3  43500  clcnvlem  43585  relpfrlem  44916  iccpartimp  47391  sbgoldbwt  47751  sbgoldbst  47752  elsetrecslem  49661