Theorem 3expib 1140

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

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

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1137	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 416	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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  df-3an 1105

This theorem is used by:  3anidm12  1447  mob  3678  dfss2  4097  eqbrrdva  5855  f1resrcmplf1dlem  7304  f1oiso2  7386  frxp  8168  onfununi  8380  smoel2  8402  smoiso2  8408  3ecoptocl  8861  ssfi  9219  f1domfi  9227  rex2dom  9275  fodomfib  9351  dffi2  9445  elfiun  9452  dif1card  10119  infxpenlem  10122  cfeq0  10364  cfsuc  10365  cfflb  10367  cfslb2n  10376  cofsmo  10377  domtriomlem  10550  axdc3lem4  10561  axdc4lem  10563  ttukey2g  10624  tskxpss  10887  grudomon  10932  elnpi  11103  dedekind  11503  nn0n0n1ge2b  12705  fzind  12827  suprzcl2  13095  icoshft  13634  fzen  13704  hashgt23el  14599  hashfundm  14617  hashbclem  14627  seqcoll  14639  relexpsucl  15216  relexpsucr  15217  relexpfld  15234  shftuz  15254  mulgcd  16753  algcvga  16786  lcmneg  16810  ressbas  17446  resseqnbas  17452  ressress  17457  psss  18786  tsrlemax  18792  isnmgm  18852  gsummgmpropd  18902  issgrpd  18951  imasgim  19516  iscmnd  20041  ring1ne0  20563  unitmulclb  20644  isdrngd  21055  isdrngdOLD  21057  abvn0b  21126  issrngd  21145  rmodislmodlem  21237  rmodislmod  21238  isphld  21993  mpfaddcl  22455  mpfmulcl  22456  pf1addcl  22704  pf1mulcl  22705  fitop  23251  hausnei2  23704  ordtt1  23730  locfincmp  23878  basqtop  24063  filfi  24211  fgcl  24230  neifil  24232  filuni  24237  cnextcn  24419  prdsmet  24722  blssps  24776  blss  24777  metcnp3  24892  hlhil  25797  volsup2  25959  sincosq1sgn  26860  sincosq2sgn  26861  sincosq3sgn  26862  sincosq4sgn  26863  sinq12ge0  26870  bcmono  27637  n0cutlt  28778  bdayfin  28906  iswlkg  30227  usgrwwlks2on  30580  umgrwwlks2on  30581  clwlkclwwlkfo  30633  loop1cycl  30777  umgr2cycllem  30779  umgr2cycl  30780  3cyclfrgrrn1  30919  grpodivf  31173  ipf  31348  shintcli  31964  spanuni  32179  adjadj  32571  unopadj2  32573  hmopadj  32574  hmopbdoptHIL  32623  resvsca  33977  resvlem  33978  submateq  34524  esumcocn  34795  bnj1379  35543  bnj571  35619  bnj594  35625  bnj580  35626  bnj600  35632  bnj1189  35722  bnj1321  35740  bnj1384  35745  trssfihf  35832  erscottd  35856  fineqvinfep  35906  trssfihfregs  35917  karddom  35942  kardsdom  35943  kardexen  35944  onprcf1acwevdlem1  36058  onvfowev  36063  cplgredgex  36075  cusgr3cyclex  36081  acycgr2v  36085  cusgracyclt3v  36091  climuzcnv  36616  elpssmo  36649  fness  37328  cgsex2gd  38263  bj-idreseq  38288  bj-imdiridlem  38311  neificl  38890  metf1o  38892  isismty  38938  ismtybndlem  38943  ablo4pnp  39017  divrngcl  39094  keridl  39169  prnc  39204  lsmsatcv  40270  llncvrlpln2  40817  lplncvrlvol2  40875  linepsubN  41012  pmapsub  41028  dalawlem10  41140  dalawlem13  41143  dalawlem14  41144  dalaw  41146  diaf11N  42309  dibf11N  42421  ismrcd1  43913  ismrcd2  43914  mzpincl  43949  mzpadd  43953  mzpmul  43954  pellfundge  44093  sqrtcval  44844  stoweidlem2  47227  stoweidlem17  47242  imaelsetpreimafv  48692  opnneir  50236  i0oii  50249  io1ii  50250