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  2446  2reu1  3883  frpoinsg  6334  ordunidif  6403  isofrlem  7329  dfwe2  7754  orduniorsuc  7811  tfisg  7836  poxp  8108  fnse  8113  ssenen  9147  dffi3  9422  fpwwe2lem12  10633  zmulcl  12608  rpneg  13003  rexuz3  15292  cau3lem  15298  climrlim2  15488  o1rlimmul  15560  iseralt  15628  gcdzeq  16491  isprm3  16617  vdwnnlem2  16928  ablfaclem3  19999  epttop  22834  lmcnp  23130  dfconn2  23245  txcnp  23446  cmphaushmeo  23626  isfild  23684  cnpflf2  23826  flimfnfcls  23854  alexsubALT  23877  fgcfil  25121  bcthlem5  25178  ivthlem2  25303  ivthlem3  25304  dvfsumrlim  25888  plypf1  26066  noetalem1  27590  noseqinds  28082  axeuclidlem  28689  usgr2wlkneq  29482  wwlksnredwwlkn0  29619  wwlksnextwrd  29620  clwlkclwwlklem2a1  29714  lnon0  30520  hstles  31953  mdsl1i  32043  atcveq0  32070  atcvat4i  32119  cdjreui  32154  issgon  33610  connpconn  34715  outsideofrflx  35594  isbasisrelowllem1  36726  isbasisrelowllem2  36727  poimirlem3  36981  poimirlem29  37007  poimir  37011  heicant  37013  equivtotbnd  37136  ismtybndlem  37164  cvrat4  38804  linepsubN  39113  pmapsub  39129  osumcllem4N  39320  pexmidlem1N  39331  dochexmidlem1  40821  cantnfresb  42563  harval3  42778  clcnvlem  42863  iccpartimp  46570  sbgoldbwt  46930  sbgoldbst  46931  elsetrecslem  47932