Theorem jctild 535

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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anc2li  565  equvini  2484  2reu1  3844  frpoinsg  6346  ordunidif  6413  isofrlem  7349  dfwe2  7789  orduniorsuc  7842  tfisg  7866  poxp  8143  fnse  8153  ssenen  9174  dffi3  9427  fpwwe2lem12  10731  zmulcl  12749  rpneg  13158  rexuz3  15522  cau3lem  15528  climrlim2  15720  o1rlimmul  15792  iseralt  15858  gcdzeq  16731  isprm3  16864  vdwnnlem2  17180  chnccat  18806  ablfaclem3  20309  epttop  23333  lmcnp  23628  dfconn2  23743  txcnp  23945  cmphaushmeo  24125  isfild  24183  cnpflf2  24325  flimfnfcls  24353  alexsubALT  24376  fgcfil  25598  bcthlem5  25655  ivthlem2  25779  ivthlem3  25780  dvfsumrlim  26357  plypf1  26537  noetalem1  28104  noseqinds  28685  axeuclidlem  29546  usgr2wlkneq  30348  wwlksnredwwlkn0  30491  wwlksnextwrd  30492  clwlkclwwlklem2a1  30589  lnon0  31406  hstles  32839  mdsl1i  32929  atcveq0  32956  atcvat4i  33005  cdjreui  33040  issgon  34802  onprcf1acwevdlem1  35965  onvfowev  35970  connpconn  36087  outsideofrflx  36985  isbasisrelowllem1  38372  isbasisrelowllem2  38373  poimirlem3  38635  poimirlem29  38661  poimir  38665  heicant  38667  equivtotbnd  38806  ismtybndlem  38834  cvrat4  40594  linepsubN  40903  pmapsub  40919  osumcllem4N  41110  pexmidlem1N  41121  dochexmidlem1  42611  cantnfresb  44420  harval3  44633  clcnvlem  44717  relpfrlem  46037  iccpartimp  48593  sbgoldbwt  48969  sbgoldbst  48970  elsetrecslem  50961