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  2487  2reu1  3852  frpoinsg  6346  ordunidif  6413  isofrlem  7340  dfwe2  7774  orduniorsuc  7827  tfisg  7851  poxp  8125  fnse  8130  ssenen  9140  dffi3  9392  fpwwe2lem12  10628  zmulcl  12644  rpneg  13051  rexuz3  15402  cau3lem  15408  climrlim2  15600  o1rlimmul  15672  iseralt  15738  gcdzeq  16611  isprm3  16742  vdwnnlem2  17057  chnccat  18683  ablfaclem3  20160  epttop  23147  lmcnp  23442  dfconn2  23557  txcnp  23758  cmphaushmeo  23938  isfild  23996  cnpflf2  24138  flimfnfcls  24166  alexsubALT  24189  fgcfil  25411  bcthlem5  25468  ivthlem2  25592  ivthlem3  25593  dvfsumrlim  26171  plypf1  26350  noetalem1  27886  noseqinds  28467  axeuclidlem  29293  usgr2wlkneq  30086  wwlksnredwwlkn0  30226  wwlksnextwrd  30227  clwlkclwwlklem2a1  30324  lnon0  31131  hstles  32564  mdsl1i  32654  atcveq0  32681  atcvat4i  32730  cdjreui  32765  issgon  34494  onvfowev  35581  connpconn  35708  outsideofrflx  36600  isbasisrelowllem1  37982  isbasisrelowllem2  37983  poimirlem3  38255  poimirlem29  38281  poimir  38285  heicant  38287  equivtotbnd  38410  ismtybndlem  38438  cvrat4  40198  linepsubN  40507  pmapsub  40523  osumcllem4N  40714  pexmidlem1N  40725  dochexmidlem1  42215  cantnfresb  44034  harval3  44247  clcnvlem  44332  relpfrlem  45645  iccpartimp  48149  sbgoldbwt  48525  sbgoldbst  48526  elsetrecslem  50460