Theorem jctild 534

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 521	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anc2li  564  equvini  2493  2reu1  3859  frpoinsg  6341  ordunidif  6408  isofrlem  7336  dfwe2  7769  orduniorsuc  7822  tfisg  7846  poxp  8120  fnse  8125  ssenen  9135  dffi3  9387  fpwwe2lem12  10623  zmulcl  12639  rpneg  13046  rexuz3  15396  cau3lem  15402  climrlim2  15594  o1rlimmul  15666  iseralt  15732  gcdzeq  16606  isprm3  16737  vdwnnlem2  17052  chnccat  18678  ablfaclem3  20155  epttop  23131  lmcnp  23426  dfconn2  23541  txcnp  23742  cmphaushmeo  23922  isfild  23980  cnpflf2  24122  flimfnfcls  24150  alexsubALT  24173  fgcfil  25395  bcthlem5  25452  ivthlem2  25576  ivthlem3  25577  dvfsumrlim  26155  plypf1  26334  noetalem1  27867  noseqinds  28448  axeuclidlem  29249  usgr2wlkneq  30042  wwlksnredwwlkn0  30182  wwlksnextwrd  30183  clwlkclwwlklem2a1  30280  lnon0  31087  hstles  32520  mdsl1i  32610  atcveq0  32637  atcvat4i  32686  cdjreui  32721  issgon  34454  onvfowev  35495  connpconn  35622  outsideofrflx  36514  isbasisrelowllem1  37884  isbasisrelowllem2  37885  poimirlem3  38157  poimirlem29  38183  poimir  38187  heicant  38189  equivtotbnd  38312  ismtybndlem  38340  cvrat4  40102  linepsubN  40411  pmapsub  40427  osumcllem4N  40618  pexmidlem1N  40629  dochexmidlem1  42119  cantnfresb  43936  harval3  44149  clcnvlem  44234  relpfrlem  45547  iccpartimp  48048  sbgoldbwt  48424  sbgoldbst  48425  elsetrecslem  50355