Theorem jctild 528

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anc2li  558  equvini  2477  2reu1  3883  ordunidif  6241  isofrlem  7095  dfwe2  7498  orduniorsuc  7547  poxp  7824  fnse  7829  ssenen  8693  dffi3  8897  fpwwe2lem13  10066  zmulcl  12034  rpneg  12424  rexuz3  14710  cau3lem  14716  climrlim2  14906  o1rlimmul  14977  iseralt  15043  gcdzeq  15904  isprm3  16029  vdwnnlem2  16334  ablfaclem3  19211  epttop  21619  lmcnp  21914  dfconn2  22029  txcnp  22230  cmphaushmeo  22410  isfild  22468  cnpflf2  22610  flimfnfcls  22638  alexsubALT  22661  fgcfil  23876  bcthlem5  23933  ivthlem2  24055  ivthlem3  24056  dvfsumrlim  24630  plypf1  24804  axeuclidlem  26750  usgr2wlkneq  27539  wwlksnredwwlkn0  27676  wwlksnextwrd  27677  clwlkclwwlklem2a1  27772  lnon0  28577  hstles  30010  mdsl1i  30100  atcveq0  30127  atcvat4i  30176  cdjreui  30211  issgon  31384  connpconn  32484  tfisg  33057  frpoinsg  33083  frmin  33086  outsideofrflx  33590  isbasisrelowllem1  34638  isbasisrelowllem2  34639  poimirlem3  34897  poimirlem29  34923  poimir  34927  heicant  34929  equivtotbnd  35058  ismtybndlem  35086  cvrat4  36581  linepsubN  36890  pmapsub  36906  osumcllem4N  37097  pexmidlem1N  37108  dochexmidlem1  38598  harval3  39911  clcnvlem  39990  iccpartimp  43584  sbgoldbwt  43949  sbgoldbst  43950  elsetrecslem  44808