Theorem expcomd 422

Description: Deduction form of expcom 419. (Contributed by Alan Sare, 22-Jul-2012.)

Hypothesis

Ref	Expression
expcomd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expcomd	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 87	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:  ancomsd  471  simplbi2comt  507  ralrimdva  3164  reupick  4278  pwssun  5551  ordelord  6383  tz7.7  6387  onelssex  6411  poxp  8130  smores2  8347  smoiun  8354  smogt  8360  tz7.49  8438  omsmolem  8649  mapxpen  9145  fodomfir  9301  f1dmvrnfibi  9312  suplub2  9435  epfrs  9714  r1sdom  9760  rankr1ai  9784  ficardom  9970  cardsdomel  9983  dfac5lem5  10134  cfsmolem  10276  cfcoflem  10278  axdc3lem2  10457  zorn2lem7  10508  genpn0  11016  reclem2pr  11061  supsrlem  11124  ltletr  11330  fzind  12723  rpneg  13080  xrltletr  13212  iccid  13447  ssfzoulel  13820  ssfzo12bi  13821  pfxccatin12lem2  14804  swrdccat  14808  repsdf2  14853  repswswrd  14859  cshwcsh2id  14903  o1rlimmul  15710  dvdsabseq  16409  divalgb  16500  bezoutlem3  16637  cncongr1  16763  ncoprmlnprm  16825  difsqpwdvds  16985  lss1d  21153  pf1ind  22586  chfacfisf  23085  chfacfisfcpmat  23086  cayleyhamilton1  23123  txlm  23880  fmfnfmlem1  24186  blsscls2  24736  metcnpi3  24778  bcmono  27521  lestr  28006  elreno2  28768  upgrewlkle2  30074  redwlk  30138  crctcshwlkn0lem5  30290  wwlksnextwrd  30373  clwwlknonex2lem2  30586  ocnel  31787  atcvat2i  32876  atcvat4i  32886  rankfilimb  35618  trssfir1om  35629  trssfir1omregs  35670  dfon2lem5  36372  cgrxfr  36643  colinearxfr  36663  hfelhf  36769  isbasisrelowllem1  38117  isbasisrelowllem2  38118  finxpreclem6  38158  seqpo  38505  atlatle  40201  cvrexchlem  40300  cvrat2  40310  cvrat4  40324  pmapjoin  40733  onfrALTlem2  45377  onfrALTlem2VD  45719  eluzge0nn0  48208  elfz2z  48211  iccpartiltu  48330  iccpartigtl  48331  iccpartlt  48332  lighneal  48522  bgoldbtbnd  48733  tgoldbach  48741  cznnring  49185  ply1mulgsumlem2  49325  itsclc0  49709