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  3845  frpoinsg  6341  ordunidif  6408  isofrlem  7341  dfwe2  7773  orduniorsuc  7826  tfisg  7850  poxp  8126  fnse  8131  ssenen  9149  dffi3  9401  fpwwe2lem12  10651  zmulcl  12667  rpneg  13076  rexuz3  15436  cau3lem  15442  climrlim2  15634  o1rlimmul  15706  iseralt  15772  gcdzeq  16642  isprm3  16773  vdwnnlem2  17088  chnccat  18714  ablfaclem3  20216  epttop  23234  lmcnp  23529  dfconn2  23644  txcnp  23846  cmphaushmeo  24026  isfild  24084  cnpflf2  24226  flimfnfcls  24254  alexsubALT  24277  fgcfil  25499  bcthlem5  25556  ivthlem2  25680  ivthlem3  25681  dvfsumrlim  26258  plypf1  26438  noetalem1  27977  noseqinds  28558  axeuclidlem  29419  usgr2wlkneq  30221  wwlksnredwwlkn0  30364  wwlksnextwrd  30365  clwlkclwwlklem2a1  30462  lnon0  31279  hstles  32712  mdsl1i  32802  atcveq0  32829  atcvat4i  32878  cdjreui  32913  issgon  34633  onvfowev  35713  connpconn  35814  outsideofrflx  36707  isbasisrelowllem1  38109  isbasisrelowllem2  38110  poimirlem3  38372  poimirlem29  38398  poimir  38402  heicant  38404  equivtotbnd  38528  ismtybndlem  38556  cvrat4  40316  linepsubN  40625  pmapsub  40641  osumcllem4N  40832  pexmidlem1N  40843  dochexmidlem1  42333  cantnfresb  44165  harval3  44378  clcnvlem  44463  relpfrlem  45776  iccpartimp  48317  sbgoldbwt  48693  sbgoldbst  48694  elsetrecslem  50625